perm filename AP[F81,JMC] blob
sn#629498 filedate 1981-12-06 generic text, type T, neo UTF8
PROVE((EQUAL (AP U (AP V U)) (AP (AP U V) U)))
Name the conjecture *1.
Let us appeal to the induction principle. Three inductions are
suggested by terms in the conjecture. They merge into two likely
candidate inductions, both of which are flawed. We limit our
consideration to the two suggested by the largest number of
nonprimitive recursive functions in the conjecture. However, one of
these is more likely than the other. We will induct according to the
following scheme:
(AND (IMPLIES (NOT (LISTP U)) (p U V))
(IMPLIES (AND (LISTP U) (p (CDR U) V))
(p U V))).
The inequality CDR.LESSP establishes that the measure (COUNT U)
decreases according to the well-founded function LESSP in the induction
step of the scheme. The above induction scheme produces the following
two new goals:
Case 2. (IMPLIES (NOT (LISTP U))
(EQUAL (AP U (AP V U))
(AP (AP U V) U))).
This simplifies, opening up the function AP, to:
T.
Case 1. (IMPLIES (AND (LISTP U)
(EQUAL (AP (CDR U) (AP V (CDR U)))
(AP (AP (CDR U) V) (CDR U))))
(EQUAL (AP U (AP V U))
(AP (AP U V) U))),
which we simplify, applying CDR.CONS, CAR.CONS, and CONS.EQUAL, and
opening up the definition of AP, to:
(IMPLIES (AND (LISTP U)
(EQUAL (AP (CDR U) (AP V (CDR U)))
(AP (AP (CDR U) V) (CDR U))))
(EQUAL (AP (CDR U) (AP V U))
(AP (AP (CDR U) V) U))).
Applying the lemma CAR/CDR.ELIM, we now replace U by (CONS Z X) to
eliminate (CDR U) and (CAR U). We must thus prove:
(IMPLIES (EQUAL (AP X (AP V X))
(AP (AP X V) X))
(EQUAL (AP X (AP V (CONS Z X)))
(AP (AP X V) (CONS Z X)))).
We will try to prove the above formula by generalizing it, replacing
(AP X V) by Y. This produces:
(IMPLIES (EQUAL (AP X (AP V X)) (AP Y X))
(EQUAL (AP X (AP V (CONS Z X)))
(AP Y (CONS Z X)))).
Give the above formula the name *1.1.
We will try to prove it by induction. The recursive terms in
the conjecture suggest six inductions. They merge into three likely
candidate inductions, two of which are unflawed. Since both of these
are equally likely, we will choose arbitrarily. We will induct
according to the following scheme:
(AND (IMPLIES (NOT (LISTP V)) (p X V Z Y))
(IMPLIES (AND (LISTP V) (p X (CDR V) Z Y))
(p X V Z Y))).
The inequality CDR.LESSP establishes that the measure (COUNT V)
decreases according to the well-founded function LESSP in the
induction step of the scheme. The above induction scheme generates
the following three new conjectures:
Case 3. (IMPLIES (AND (NOT (LISTP V))
(EQUAL (AP X (AP V X)) (AP Y X)))
(EQUAL (AP X (AP V (CONS Z X)))
(AP Y (CONS Z X)))),
which simplifies, opening up AP, to:
(IMPLIES (AND (NOT (LISTP V))
(EQUAL (AP X X) (AP Y X)))
(EQUAL (AP X (CONS Z X))
(AP Y (CONS Z X)))),
which has an irrelevant term in it. By eliminating the term we get:
(IMPLIES (EQUAL (AP X X) (AP Y X))
(EQUAL (AP X (CONS Z X))
(AP Y (CONS Z X)))),
which we will name *1.1.1.
Case 2. (IMPLIES (AND (LISTP V)
(NOT (EQUAL (AP X (AP (CDR V) X))
(AP Y X)))
(EQUAL (AP X (AP V X)) (AP Y X)))
(EQUAL (AP X (AP V (CONS Z X)))
(AP Y (CONS Z X)))),
which we simplify, expanding the definition of AP, to:
collecting lists
10207, 10207 free cells
(IMPLIES (AND (LISTP V)
(NOT (EQUAL (AP X (AP (CDR V) X))
(AP Y X)))
(EQUAL (AP X (CONS (CAR V) (AP (CDR V) X)))
(AP Y X)))
(EQUAL (AP X
(CONS (CAR V)
(AP (CDR V) (CONS Z X))))
(AP Y (CONS Z X)))).
Appealing to the lemma CAR/CDR.ELIM, replace V by (CONS D W) to
eliminate (CDR V) and (CAR V). This produces:
(IMPLIES (AND (NOT (EQUAL (AP X (AP W X)) (AP Y X)))
(EQUAL (AP X (CONS D (AP W X)))
(AP Y X)))
(EQUAL (AP X (CONS D (AP W (CONS Z X))))
(AP Y (CONS Z X)))).
We use the above equality hypothesis by substituting
(AP X (CONS D (AP W X))) for (AP Y X) and throwing away the
equality. We must thus prove:
(IMPLIES (NOT (EQUAL (AP X (AP W X))
(AP X (CONS D (AP W X)))))
(EQUAL (AP X (CONS D (AP W (CONS Z X))))
(AP Y (CONS Z X)))),
which we generalize by replacing (AP W X) by A. This produces:
(IMPLIES (NOT (EQUAL (AP X A) (AP X (CONS D A))))
(EQUAL (AP X (CONS D (AP W (CONS Z X))))
(AP Y (CONS Z X)))),
which we will name *1.1.2.
Case 1. (IMPLIES (AND (LISTP V)
(EQUAL (AP X (AP (CDR V) (CONS Z X)))
(AP Y (CONS Z X)))
(EQUAL (AP X (AP V X)) (AP Y X)))
(EQUAL (AP X (AP V (CONS Z X)))
(AP Y (CONS Z X)))).
This simplifies, expanding AP, to:
(IMPLIES (AND (LISTP V)
(EQUAL (AP X (AP (CDR V) (CONS Z X)))
(AP Y (CONS Z X)))
(EQUAL (AP X (CONS (CAR V) (AP (CDR V) X)))
(AP Y X)))
(EQUAL (AP X
(CONS (CAR V)
(AP (CDR V) (CONS Z X))))
(AP Y (CONS Z X)))).
Applying the lemma CAR/CDR.ELIM, we now replace V by (CONS D W) to
eliminate (CDR V) and (CAR V). We would thus like to prove the
conjecture:
(IMPLIES (AND (EQUAL (AP X (AP W (CONS Z X)))
(AP Y (CONS Z X)))
(EQUAL (AP X (CONS D (AP W X)))
(AP Y X)))
(EQUAL (AP X (CONS D (AP W (CONS Z X))))
(AP Y (CONS Z X)))).
We use the first equality hypothesis by substituting
(AP X (AP W (CONS Z X))) for (AP Y (CONS Z X)) and throwing away
the equality. We would thus like to prove:
(IMPLIES (EQUAL (AP X (CONS D (AP W X)))
(AP Y X))
(EQUAL (AP X (CONS D (AP W (CONS Z X))))
(AP X (AP W (CONS Z X))))).
We will try to prove the above formula by generalizing it,
replacing (AP W (CONS Z X)) by A. We restrict the new variable by
recalling the type restriction lemma noted when AP was introduced.
This produces:
(IMPLIES (AND (LISTP A)
(EQUAL (AP X (CONS D (AP W X)))
(AP Y X)))
(EQUAL (AP X (CONS D A)) (AP X A))).
Give the above formula the name *1.1.3.
We will appeal to induction. The recursive terms in the
conjecture suggest five inductions. They merge into three likely
candidate inductions, two of which are unflawed. Since both of
these are equally likely, we will choose arbitrarily. We will
induct according to the following scheme:
(AND (IMPLIES (NOT (LISTP W))
(p X D A W Y))
(IMPLIES (AND (LISTP W) (p X D A (CDR W) Y))
(p X D A W Y))).
The inequality CDR.LESSP establishes that the measure (COUNT W)
decreases according to the well-founded function LESSP in the
induction step of the scheme. The above induction scheme produces
the following two new conjectures:
Case 2. (IMPLIES (AND (NOT (LISTP W))
(LISTP A)
(EQUAL (AP X (CONS D (AP W X)))
(AP Y X)))
(EQUAL (AP X (CONS D A)) (AP X A))).
This simplifies, expanding the function AP, to:
(IMPLIES (AND (NOT (LISTP W))
(LISTP A)
(EQUAL (AP X (CONS D X)) (AP Y X)))
(EQUAL (AP X (CONS D A)) (AP X A))).
Eliminate the irrelevant term. The result is:
(IMPLIES (AND (LISTP A)
(EQUAL (AP X (CONS D X)) (AP Y X)))
(EQUAL (AP X (CONS D A)) (AP X A))),
which we will name *1.1.3.1.
Case 1. (IMPLIES (AND (LISTP W)
(NOT (EQUAL (AP X (CONS D (AP (CDR W) X)))
(AP Y X)))
(LISTP A)
(EQUAL (AP X (CONS D (AP W X)))
(AP Y X)))
(EQUAL (AP X (CONS D A)) (AP X A))),
which simplifies, opening up the definition of AP, to:
(IMPLIES
(AND (LISTP W)
(NOT (EQUAL (AP X (CONS D (AP (CDR W) X)))
(AP Y X)))
(LISTP A)
(EQUAL (AP X
(CONS D
(CONS (CAR W) (AP (CDR W) X))))
(AP Y X)))
(EQUAL (AP X (CONS D A)) (AP X A))).
Appealing to the lemma CAR/CDR.ELIM, we now replace W by
(CONS V Z) to eliminate (CDR W) and (CAR W). This produces:
collecting lists
10008, 10008 free cells
(IMPLIES (AND (NOT (EQUAL (AP X (CONS D (AP Z X)))
(AP Y X)))
(LISTP A)
(EQUAL (AP X (CONS D (CONS V (AP Z X))))
(AP Y X)))
(EQUAL (AP X (CONS D A)) (AP X A))).
We use the above equality hypothesis by substituting:
(AP X (CONS D (CONS V (AP Z X))))
for (AP Y X) and throwing away the equality. We would thus like
to prove:
(IMPLIES
(AND (NOT (EQUAL (AP X (CONS D (AP Z X)))
(AP X (CONS D (CONS V (AP Z X))))))
(LISTP A))
(EQUAL (AP X (CONS D A)) (AP X A))).
We will try to prove the above formula by generalizing it,
replacing (AP Z X) by U. This produces:
(IMPLIES (AND (NOT (EQUAL (AP X (CONS D U))
(AP X (CONS D (CONS V U)))))
(LISTP A))
(EQUAL (AP X (CONS D A)) (AP X A))).
Call the above conjecture *1.1.3.2.
We will try to prove it by induction. There are four
plausible inductions. However, they merge into one likely
candidate induction. We will induct according to the following
scheme:
(AND (IMPLIES (NOT (LISTP X))
(p X D A U V))
(IMPLIES (AND (LISTP X) (p (CDR X) D A U V))
(p X D A U V))).
The inequality CDR.LESSP establishes that the measure (COUNT X)
decreases according to the well-founded function LESSP in the
induction step of the scheme. The above induction scheme
generates the following three new conjectures:
Case 3. (IMPLIES (AND (NOT (LISTP X))
(NOT (EQUAL (AP X (CONS D U))
(AP X (CONS D (CONS V U)))))
(LISTP A))
(EQUAL (AP X (CONS D A)) (AP X A))),
which we simplify, rewriting with CONS.EQUAL, and expanding the
definition of AP, to:
(IMPLIES (NOT (LISTP X))
(NOT (LISTP A))).
Eliminate irrelevant terms. This generates:
F.
Why say more?
************** F A I L E D **************
NIL
8←